feat(fields): add fast Mersenne31 arithmetic by varunthakore · Pull Request #257 · Verified-zkEVM/CompPoly

varunthakore · 2026-06-23T06:46:04Z

No description provided.

github-actions · 2026-06-23T06:47:46Z

🤖 PR Summary

Overview

This PR restructures the Mersenne31 field implementation and adds a fast, UInt32-backed arithmetic core. The module is split from a single file into a subdirectory with three components: a facade, a canonical ZMod-based definition, and a native-word implementation.

Restructuring

The old CompPoly/Fields/Mersenne.lean has been deleted. It previously held the Mersenne31 namespace, a reducible fieldSize definition, Field as ZMod fieldSize, and a primality proof via the pratt tactic. These definitions have been removed from the project.
A new facade CompPoly/Fields/Mersenne31.lean provides a single entry point that re-exports both the ZMod model and the fast implementation.
The file CompPoly.lean was updated to import the new module structure.

Mathematical Formalization

CompPoly/Fields/Mersenne31/Basic.lean defines the Mersenne31 prime field 2^31 - 1 as used in Circle STARKs. It provides:
- fieldSize : ℕ := 2^31 - 1
- Field : Type as ZMod fieldSize
- is_prime : Nat.Prime fieldSize, proved via a Pratt certificate
- Fact (Nat.Prime fieldSize) and Field instance
- NonBinaryField instance (characteristic ≠ 2)

Fast Arithmetic Implementation

CompPoly/Fields/Mersenne31/Fast.lean (994 lines) introduces a UInt32-backed carrier Fast.Field as a subtype of UInt32 with toNat < fieldSize. It implements add, sub, neg, mul, inv, div, and pow, reducing intermediate UInt32 or UInt64 results via the Mersenne identity 2^31 ≡ 1 mod p.
Correctness is established via a ring isomorphism ringEquiv : Fast.Field ≃+* Basic.Field (the canonical ZMod model), using toField_injective.field. The toField_* morphism theorems verify the arithmetic.
A Field instance and instNonBinaryField (showing 2 ≠ 0) are provided.

No sorry or admit placeholders are present in any of the new or modified files.

Statistics

Metric	Count
📝 Files Changed	5
✅ Lines Added	1059
❌ Lines Removed	27

Lean Declarations

✏️ Removed: 3 declaration(s)

CompPoly/Fields/Mersenne.lean (3)

abbrev Field
def fieldSize : Nat
theorem is_prime : Nat.Prime fieldSize

✏️ Added: 108 declaration(s)

CompPoly/Fields/Mersenne31/Basic.lean (3)

abbrev Field
def fieldSize : Nat
theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/Mersenne31/Fast.lean (105)

abbrev Field : Type
def add (x y : Field) : Field
def div (x y : Field) : Field
def inv (x : Field) : Field
def modulus : UInt32
def mul (x y : Field) : Field
def neg (x : Field) : Field
def ofField (x : Mersenne31.Basic.Field) : Field
def ofInt (z : Int) : Field
def ofNat (n : Nat) : Field
def ofUInt32 (x : UInt32) : Field
def pow (x : Field) (n : Nat) : Field
def raw (x : Field) : UInt32
def ringEquiv : Field ≃+* Mersenne31.Basic.Field where
def square (x : Field) : Field
def sub (x y : Field) : Field
def toField (x : Field) : Mersenne31.Basic.Field
def toNat (x : Field) : Nat
instance instAddField : Add Field where
instance instDivField : Div Field where
instance instIntCastField : IntCast Field where
instance instIntSMulField : SMul Int Field where
instance instInvField : Inv Field where
instance instMulField : Mul Field where
instance instNNRatCastField : NNRatCast Field where
instance instNNRatSMulField : SMul ℚ≥0 Field where
instance instNatCastField : NatCast Field where
instance instNatSMulField : SMul Nat Field where
instance instNegField : Neg Field where
instance instOneField : One Field where
instance instPowFieldInt : Pow Field Int where
instance instPowFieldNat : Pow Field Nat where
instance instRatCastField : RatCast Field where
instance instRatSMulField : SMul ℚ Field where
instance instSubField : Sub Field where
instance instZeroField : Zero Field where
private def invExponent : Nat
private def modulus64 : UInt64
private def ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) : Field
private def one : Field
private def reduceUInt32Lt2Modulus (x : UInt32)
private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32
private def reduceUInt64 (x : UInt64)
private def reduceUInt64Raw (x : UInt64) : UInt32
private def shift4Mul (acc digit : Field) : Field
private def zero : Field
private theorem fieldSize_add_fieldSize_lt_uint32Size :
private theorem fieldSize_lt_uint32Size : Mersenne31.Basic.fieldSize < UInt32.size
private theorem fieldSize_mul_fieldSize_lt_two64 :
private theorem fieldSize_pos : 0 < Mersenne31.Basic.fieldSize
private theorem modulus64_toNat : modulus64.toNat = Mersenne31.Basic.fieldSize
private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z)
private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x
private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32)
private theorem reduceUInt32Lt2Modulus_cast (x : UInt32)
private theorem reduceUInt64Raw_lt (x : UInt64)
private theorem reduceUInt64Raw_split_toNat (x : UInt64)
private theorem reduceUInt64_cast (x : UInt64)
private theorem toField_injective : Function.Injective toField
private theorem toField_inv_pow (x : Field) :
private theorem toField_mul_pow (base x y : Field) (m n : Nat)
private theorem toField_ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) :
private theorem toField_reduceUInt64 (x : UInt64)
private theorem toField_shift4Mul (acc digit : Field) :
private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat)
private theorem toNat_ofCanonicalNat (n : Nat) (h : n < Mersenne31.Basic.fieldSize) :
theorem modulus_toNat : modulus.toNat = Mersenne31.Basic.fieldSize
theorem ofField_toField (x : Field) :
theorem raw_eq_val (x : Field) : raw x = x.val
theorem raw_mk (x : UInt32) (h : x.toNat < Mersenne31.Basic.fieldSize) :
theorem raw_one : raw (1 : Field) = 1
theorem raw_zero : raw (0 : Field) = 0
theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
theorem ringEquiv_symm_apply (x : Mersenne31.Basic.Field) : ringEquiv.symm x = ofField x
theorem toField_add (x y : Field) :
theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y
theorem toField_intCast (n : Int) :
theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹
theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y
theorem toField_natCast (n : Nat) :
theorem toField_neg (x : Field) : toField (-x) = -toField x
theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x
theorem toField_nnratCast (q : ℚ≥0) :
theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n
theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x
theorem toField_ofField (x : Mersenne31.Basic.Field) :
theorem toField_ofInt (z : Int) :
theorem toField_ofNat (n : Nat) :
theorem toField_ofUInt32 (x : UInt32) :
theorem toField_one : toField (1 : Field) = 1
theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n
theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x
theorem toField_ratCast (q : ℚ) :
theorem toField_square (x : Field) : toField (square x) = toField x * toField x
theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y
theorem toField_zero : toField (0 : Field) = 0
theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n
theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x
theorem toNat_eq_val_toNat (x : Field) : toNat x = x.val.toNat
theorem toNat_mk (x : UInt32) (h : x.toNat < Mersenne31.Basic.fieldSize) :
theorem toNat_ofField (x : Mersenne31.Basic.Field) : toNat (ofField x) = x.val
theorem toNat_ofNat (n : Nat) :
theorem toNat_ofUInt32 (x : UInt32) :
theorem toNat_one : toNat (1 : Field) = 1
theorem toNat_zero : toNat (0 : Field) = 0

sorry Tracking

No sorrys were added, removed, or affected.

📋 **Additional Analysis**

The diff implements a significant refactoring/improvement (replacing the single Mersenne.lean file with a structured Mersenne31/ subdirectory containing Basic.lean and Fast.lean). The analysis covers the diff's adherence to the provided guidelines, identifying compliance with most major points (title format, licensing, file/copyright, naming conventions, module layout, proof placement, deprecation handling, imports, documentation structure) but noting specific issues: variable naming inconsistency for hsum_lt_uint32 (should be hsum_lt_uint32Size), missing citation entry in blueprint/src/references.bib for any paper describing the fast reduction algorithm, and a minor style-preference issue regarding leaving non-terminal simp calls unsqueezed. Two time commands discovered two compliance fixes: the simp after toField_div can stay unsqueezed (it's terminal), and there is a correct deprecation alias was added (dominated by the removal).

📄 **Per-File Summaries**

CompPoly.lean: Replaced the single import of CompPoly.Fields.Mersenne with three imports: CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast. This restructures the Mersenne field module from a single file into a subdirectory containing a basic definition file and a fast operations file, improving modularity.
CompPoly/Fields/Mersenne.lean: The file CompPoly/Fields/Mersenne.lean was deleted, removing the Mersenne31 namespace along with the reducible definition fieldSize : Nat := 2 ^ 31 - 1, the abbreviation Field := ZMod fieldSize, and the theorem is_prime : Nat.Prime fieldSize (proved via the pratt tactic). This eliminates the Mersenne‑31 prime field construction used in Circle STARKs from the project.
CompPoly/Fields/Mersenne31.lean: Added a new facade module CompPoly/Fields/Mersenne31.lean that imports and re-exports the canonical ZMod model of the Mersenne31 prime field (2^{31} - 1) from CompPoly.Fields.Mersenne31.Basic and the native-word implementation from CompPoly.Fields.Mersenne31.Fast. This module provides a single entry point for users of the Mersenne31 field.
CompPoly/Fields/Mersenne31/Basic.lean: Added CompPoly/Fields/Mersenne31/Basic.lean, which defines the Mersenne31 prime field 2³¹-1 used in Circle STARKs. It introduces fieldSize as 2^31 - 1, Field as ZMod fieldSize, proves is_prime via a Pratt certificate, and registers Fact (Nat.Prime fieldSize) and a Field instance. It also provides a NonBinaryField instance showing the field has characteristic different from 2.
CompPoly/Fields/Mersenne31/Fast.lean: This new file (994 lines) introduces Mersenne31.Fast, a UInt32-backed implementation of the Mersenne31 prime field (2^31 - 1). It defines the carrier abbrev Field as the subtype of UInt32 with toNat < fieldSize and provides arithmetic operations (add, sub, neg, mul, inv, div, pow) that reduce intermediate UInt32 or UInt64 results using the Mersenne identity 2^31 ≡ 1 mod p. The file establishes a Field instance via a ring equivalence ringEquiv : Field ≃+* Mersenne31.Basic.Field (the canonical ZMod model) using toField_injective.field, and demonstrates correctness through toField_* morphism theorems. It also provides instNonBinaryField showing 2 ≠ 0. No sorry or admit are present.

Last updated: 2026-07-20 08:30 UTC.

MavenRain

A couple of things:

Consider adding tests for Mersenne31.Fast
Mersenne.lean is still referenced in the docs. Consider updating.
Consider extracting the four have blocks duplicated between reduceUInt64_cast and reduceUInt64Raw_lt into a private lemma.

dhsorens

Summary

Solid Fast track: Mersenne reduction (not Montgomery) is the right call for 2^31-1, and the toField_* / ringEquiv / inv addition-chain proofs are in good shape.

Blockers before merge: green CI, rebase onto current main, and a #guard test file matching BabyBear/KoalaBear Fast.

Inline notes are the actionable items.

github-actions · 2026-08-24T22:34:38Z

🤖 PR Summary

This pull request adds a fully formalized and verified implementation of the Mersenne31 prime field (2^31 - 1) for use in Circle STARKs, along with a fast UInt32-backed representation, a refactored module structure with backward compatibility, and comprehensive test coverage. The core changes are in the new Mersenne31/Basic.lean and Mersenne31/Fast.lean files; the remaining files are either module re-exports, a deprecation shim, or test integration files. No sorry or admit placeholders are introduced.

Statistics

Metric	Count
📝 Files Changed	8
✅ Lines Added	1105
❌ Lines Removed	19

Lean Declarations

✏️ Removed: 3 declaration(s)

CompPoly/Fields/Mersenne.lean (3)

abbrev Field
def fieldSize : Nat
theorem is_prime : Nat.Prime fieldSize

✏️ Added: 107 declaration(s)

CompPoly/Fields/Mersenne31/Basic.lean (3)

abbrev Field
def fieldSize : Nat
theorem is_prime : Nat.Prime fieldSize

CompPoly/Fields/Mersenne31/Fast.lean (104)

abbrev Field : Type
def add (x y : Field) : Field
def div (x y : Field) : Field
def inv (x : Field) : Field
def modulus : UInt32
def mul (x y : Field) : Field
def neg (x : Field) : Field
def ofField (x : Mersenne31.Field) : Field
def ofInt (z : Int) : Field
def ofNat (n : Nat) : Field
def ofUInt32 (x : UInt32) : Field
def pow (x : Field) (n : Nat) : Field
def raw (x : Field) : UInt32
def ringEquiv : Field ≃+* Mersenne31.Field where
def square (x : Field) : Field
def sub (x y : Field) : Field
def toField (x : Field) : Mersenne31.Field
def toNat (x : Field) : Nat
instance instAddField : Add Field where
instance instDivField : Div Field where
instance instIntCastField : IntCast Field where
instance instIntSMulField : SMul Int Field where
instance instInvField : Inv Field where
instance instMulField : Mul Field where
instance instNNRatCastField : NNRatCast Field where
instance instNNRatSMulField : SMul ℚ≥0 Field where
instance instNatCastField : NatCast Field where
instance instNatSMulField : SMul Nat Field where
instance instNegField : Neg Field where
instance instOneField : One Field where
instance instPowFieldInt : Pow Field Int where
instance instPowFieldNat : Pow Field Nat where
instance instRatCastField : RatCast Field where
instance instRatSMulField : SMul ℚ Field where
instance instSubField : Sub Field where
instance instZeroField : Zero Field where
private def invExponent : Nat
private def modulus64 : UInt64
private def ofCanonicalNat (n : Nat) (h : n < Mersenne31.fieldSize) : Field
private def reduceUInt32Lt2Modulus (x : UInt32)
private def reduceUInt32Lt2ModulusRaw (x : UInt32) : UInt32
private def reduceUInt64 (x : UInt64)
private def reduceUInt64Raw (x : UInt64) : UInt32
private def shift4Mul (acc digit : Field) : Field
private theorem fieldSize_add_fieldSize_lt_uint32Size :
private theorem fieldSize_lt_uint32Size : Mersenne31.fieldSize < UInt32.size
private theorem fieldSize_mul_fieldSize_lt_two64 :
private theorem fieldSize_pos : 0 < Mersenne31.fieldSize
private theorem modulus64_toNat : modulus64.toNat = Mersenne31.fieldSize
private theorem mul_assoc_field (x y z : Field) : (x * y) * z = x * (y * z)
private theorem pow_succ (x : Field) (n : Nat) : pow x (n + 1) = pow x n * x
private theorem reduceUInt32Lt2ModulusRaw_lt (x : UInt32)
private theorem reduceUInt32Lt2Modulus_cast (x : UInt32)
private theorem reduceUInt64Raw_lt (x : UInt64)
private theorem reduceUInt64Raw_split_toNat (x : UInt64)
private theorem reduceUInt64_cast (x : UInt64)
private theorem reduceUInt64_split_sum_bounds (x : UInt64)
private theorem toField_injective : Function.Injective toField
private theorem toField_inv_pow (x : Field) :
private theorem toField_mul_pow (base x y : Field) (m n : Nat)
private theorem toField_ofCanonicalNat (n : Nat) (h : n < Mersenne31.fieldSize) :
private theorem toField_reduceUInt64 (x : UInt64)
private theorem toField_shift4Mul (acc digit : Field) :
private theorem toField_shift4Mul_pow (base acc digit : Field) (e d : Nat)
private theorem toNat_ofCanonicalNat (n : Nat) (h : n < Mersenne31.fieldSize) :
theorem modulus_toNat : modulus.toNat = Mersenne31.fieldSize
theorem ofField_toField (x : Field) :
theorem raw_eq_val (x : Field) : raw x = x.val
theorem raw_mk (x : UInt32) (h : x.toNat < Mersenne31.fieldSize) :
theorem raw_one : raw (1 : Field) = 1
theorem raw_zero : raw (0 : Field) = 0
theorem ringEquiv_apply (x : Field) : ringEquiv x = toField x
theorem ringEquiv_symm_apply (x : Mersenne31.Field) : ringEquiv.symm x = ofField x
theorem toField_add (x y : Field) :
theorem toField_div (x y : Field) : toField (x / y) = toField x / toField y
theorem toField_intCast (n : Int) :
theorem toField_inv (x : Field) : toField x⁻¹ = (toField x)⁻¹
theorem toField_mul (x y : Field) : toField (x * y) = toField x * toField y
theorem toField_natCast (n : Nat) :
theorem toField_neg (x : Field) : toField (-x) = -toField x
theorem toField_nnqsmul (q : ℚ≥0) (x : Field) : toField (q • x) = q • toField x
theorem toField_nnratCast (q : ℚ≥0) :
theorem toField_npow (x : Field) (n : Nat) : toField (x ^ n) = toField x ^ n
theorem toField_nsmul (n : Nat) (x : Field) : toField (n • x) = n • toField x
theorem toField_ofField (x : Mersenne31.Field) :
theorem toField_ofInt (z : Int) :
theorem toField_ofNat (n : Nat) :
theorem toField_ofUInt32 (x : UInt32) :
theorem toField_one : toField (1 : Field) = 1
theorem toField_pow (x : Field) (n : Nat) : toField (pow x n) = toField x ^ n
theorem toField_qsmul (q : ℚ) (x : Field) : toField (q • x) = q • toField x
theorem toField_ratCast (q : ℚ) :
theorem toField_square (x : Field) : toField (square x) = toField x * toField x
theorem toField_sub (x y : Field) : toField (x - y) = toField x - toField y
theorem toField_zero : toField (0 : Field) = 0
theorem toField_zpow (x : Field) (n : Int) : toField (x ^ n) = toField x ^ n
theorem toField_zsmul (n : Int) (x : Field) : toField (n • x) = n • toField x
theorem toNat_eq_val_toNat (x : Field) : toNat x = x.val.toNat
theorem toNat_mk (x : UInt32) (h : x.toNat < Mersenne31.fieldSize) :
theorem toNat_ofField (x : Mersenne31.Field) : toNat (ofField x) = x.val
theorem toNat_ofNat (n : Nat) :
theorem toNat_ofUInt32 (x : UInt32) :
theorem toNat_one : toNat (1 : Field) = 1
theorem toNat_zero : toNat (0 : Field) = 0

sorry Tracking

No sorrys were added, removed, or affected.

📄 **Per-File Summaries**

CompPoly.lean: The diff adds three public import lines for CompPoly.Fields.Mersenne31, CompPoly.Fields.Mersenne31.Basic, and CompPoly.Fields.Mersenne31.Fast to the top-level CompPoly.lean module. This exposes the new Mersenne31 field implementation and its fast arithmetic routines as part of the library's public API.
CompPoly/Fields/Mersenne.lean: The file CompPoly/Fields/Mersenne.lean was entirely rewritten from defining the Mersenne31 field (including fieldSize, Field abbreviation, and the is_prime theorem proven via pratt) into a deprecated compatibility shim. It now only re-exports CompPoly.Fields.Mersenne31 via a public import, adds a deprecated_module annotation directing users to the new import path, and updates the author list to include Varun Thakore. This change moves the primary definition to a dedicated module while preserving backward compatibility for existing imports.
CompPoly/Fields/Mersenne31.lean: Added a new facade module CompPoly/Fields/Mersenne31.lean that re-exports the canonical ZMod model from CompPoly.Fields.Mersenne31.Basic and the native-word implementation from CompPoly.Fields.Mersenne31.Fast, via two public import statements and an @[expose] public section. This provides a single entry point for users of the Mersenne31 prime field (2^31 - 1). No sorry or admit are present.
CompPoly/Fields/Mersenne31/Basic.lean: This new file (CompPoly/Fields/Mersenne31/Basic.lean) introduces the Mersenne31 prime field 2^31 - 1 for use in Circle STARKs. It defines fieldSize as 2 ^ 31 - 1, sets Field as ZMod fieldSize, and proves primality via pratt (a Pratt certificate tactic). It then provides the necessary instances for the field structure: Fact (Nat.Prime fieldSize), _root_.Field Field via ZMod.instField, and NonBinaryField Field with a char_neq_2 proof discharged by decide.
CompPoly/Fields/Mersenne31/Fast.lean: This file adds a new Fast namespace under Mersenne31 providing a Field type that stores canonical UInt32 representatives below the Mersenne-31 prime 2^31-1. It defines conversion functions (ofNat, toNat, ofField, toField, ofUInt32, ofInt) and instances for the standard arithmetic operations (Add, Sub, Neg, Mul, Inv, Div, Pow, and scalar multiplication), each accompanied by toField_* theorems that prove they agree with the canonical Mersenne31.Field (the ZMod model). Efficient reduction strategies are implemented: addition and subtraction use conditional subtraction or addition of the modulus, multiplication reduces a UInt64 product via the Mersenne identity (split at bit 31, add halves, then UInt32 reduce), and inversion uses a fixed Fermat addition chain for the exponent p-2. The file finishes by transferring the field structure using toField_injective.field, producing Field, CommRing, and NonBinaryField instances on the fast type, and exports a ringEquiv : Field ≃+* Mersenne31.Field. No sorry or admit are present.
CompPoly/Fields/README.md: Added entries documenting the new Mersenne31.lean facade, Mersenne31/Basic.lean (canonical field model and primality proof), and Mersenne31/Fast.lean (verified UInt32 implementation). The old Mersenne.lean entry is now tagged as a deprecated compatibility re-export, retained for existing imports. This gives readers a clear inventory of the refactored Mersenne31 module and its deprecation path.
tests/CompPolyTests.lean: The diff adds a single public import line for CompPolyTests.Fields.Mersenne31.Fast to the test file's import block. This makes the tests and definitions from that module available, integrating Mersenne31 field arithmetic into the overall test suite.
tests/CompPolyTests/Fields/Mersenne31/Fast.lean: Added a new test file tests/CompPolyTests/Fields/Mersenne31/Fast.lean containing regression checks for the executable native-word representation of the Mersenne31 field defined in CompPoly.Fields.Mersenne31.Fast. The #guard statements verify that the fast implementation produces correct val, toNat, toField, and arithmetic results (+, -, *, ^, ⁻¹, /) on edge cases such as zero, one, field size wrapping, multiplicative inverse, and exponentiation with negative exponent, and cross-check these against the reference Mersenne31.Field behavior. No sorry or admit are present.

Last updated: 2026-09-01 18:55 UTC.

dhsorens

All requested review changes are addressed. The generated compatibility import is restored, and local build, tests, style lint, documentation integrity, and import validation pass on the merged-main head.

dhsorens · 2026-09-01T19:04:39Z

thanks @varunthakore for the contribution!

This was referenced Jun 26, 2026

[codex] Add Mersenne31 regression tests for PR 257 adrienlacombe/CompPoly#2

Draft

feat(fields): add Mersenne31 circle domain skeleton adrienlacombe/CompPoly#3

Draft

test(fields): extend Mersenne31 regression coverage #260

Open

MavenRain approved these changes Jun 28, 2026

View reviewed changes

dhsorens requested changes Jul 31, 2026

View reviewed changes

Comment thread CompPoly/Fields/Mersenne31/Fast.lean Outdated

Comment thread CompPoly/Fields/Mersenne31/Basic.lean Outdated

Comment thread CompPoly/Fields/Mersenne31/Fast.lean Outdated

Comment thread CompPoly/Fields/Mersenne31/Fast.lean

Comment thread CompPoly/Fields/Mersenne31.lean

varunthakore added 3 commits August 24, 2026 18:32

feat(fields): add Mersenne31 field scaffold

26213cc

feat(fields): implement fast Mersenne31 arithmetic

c04266d

chore(fields): add comments

3f3e409

varunthakore force-pushed the mersenne31 branch from 8b16d84 to 3f3e409 Compare August 24, 2026 22:32

varunthakore and others added 5 commits August 25, 2026 17:49

refactor(fields): modularize Mersenne31 basic and fast implementations

f0c0a3f

doc(fields): add Mersenne31 to readme

34021d7

test(fields): add Mersenne31 tests

5068d4c

Merge branch 'main' into mersenne31

d6e4881

fix(fields): export Mersenne compatibility module

4f57ff2

dhsorens approved these changes Sep 1, 2026

View reviewed changes

dhsorens enabled auto-merge (squash) September 1, 2026 18:41

Merge branch 'main' into mersenne31

1a7a8e5

dhsorens merged commit ba5032e into Verified-zkEVM:main Sep 1, 2026
5 checks passed

adrienlacombe mentioned this pull request Sep 1, 2026

feat(fields): add Mersenne31 circle domain skeleton #310

Draft

Navigation Menu

Uh oh!

feat(fields): add fast Mersenne31 arithmetic - #257

feat(fields): add fast Mersenne31 arithmetic#257
dhsorens merged 9 commits into
Verified-zkEVM:mainfrom
varunthakore:mersenne31

varunthakore commented Jun 23, 2026

Uh oh!

github-actions Bot commented Jun 23, 2026 •

edited

Loading

Uh oh!

MavenRain left a comment

Uh oh!

dhsorens left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented Aug 24, 2026 •

edited

Loading

Uh oh!

dhsorens left a comment

Uh oh!

Uh oh!

dhsorens commented Sep 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

varunthakore commented Jun 23, 2026

Uh oh!

github-actions Bot commented Jun 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Overview

Restructuring

Mathematical Formalization

Fast Arithmetic Implementation

Uh oh!

MavenRain left a comment

Choose a reason for hiding this comment

Uh oh!

dhsorens left a comment

Choose a reason for hiding this comment

Summary

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

github-actions Bot commented Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

dhsorens left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

dhsorens commented Sep 1, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

github-actions Bot commented Jun 23, 2026 •

edited

Loading

github-actions Bot commented Aug 24, 2026 •

edited

Loading